\section{Running Example (Naive Version)}
\label{sec:Running}

\begin{figure}[t]%
	\includegraphics[width=\columnwidth]{images/NaiveFS-MM.png}%
	\vspace{-0.3cm}
	\caption{Simplified \textsc{Mls} metamodel \cite{Bell:Lapadula:73}, as a Kermeta Class Diagram \cite{Kermeta-Weaving2005}.}%
	\label{fig:MLS-MM}%
		\vspace{-0.5cm}
\end{figure}

Our example is inspired from \cite{ASSE:Cristia}: it is an \textsc{Unix}-like operating system that includes a Multi-Level Security (\textsc{Mls}) File System (\textsc{Fs}). We first present the expected requirements on the file system, then explain its implementation in terms of \textsc{Apn}, and finish with the requirements formalisation in terms of three properties expressed over the \textsc{Apn}. \Sect \ref{sec:Evolving} will then present two manual evolution that iteratively enforce more properties on the system.

\input{Requirements}
\input{MC}
\input{NFS}
\input{RP}
